Key:
Save
Speagram Home
|
tutorial
|
use me
|
live interface
|
documentation
|
developer's corner
|
links
|
contact
FUNCTIONAL PROGRAMMING ON TOP OF SPEAGRAM
Done
Hide
Edit
Run
This part
New
Up
Down
Delete
Help
…
TEMPLAT_TEXT
Done
Hide
Edit
Run
This part
New
Up
Down
Delete
Help
…
Speagram can serve as a full-status functional programming language because any program written in a functional language can be thought of as a system of rewrite rules. We recommend to use syntax similar to natural language in Speagram because in this way you can use Speagram as an advanced parser. But we also created ''Sasha'' — a set of syntax rules written on top of Speagram to allow you to write Speagram functions with the syntax of a typical functional programming language. You observed that we normally use dot . as a delimiter in Speagram, but in this context we are going to use semicolon ; as it seems better suited.
Done
Hide
Edit
Run
This part
New
Up
Down
Delete
Help
…
Before we show you how Sasha is created on top of Speagram let us write a simple function in Sasha so you can see how it looks like. %$ Load state library:/sasha. fun fib (x : nat) : nat; fib (0) => 0; fib (1) => 1; fib (x) => fib (x - 2) + fib (x - 1); ***; fib (7); $%
Done
Hide
Edit
Run
This part
New
Up
Down
Delete
Help
…
To be able to parse Sasha on top of Speagram we must first make Speagram accept function definitions given in Sasha as it's internal definitions. This is possible because Speagram does not impose it's internal syntax on you, you can change it using shorthand as you will see. The first part of the work is to give new way to define functions. Normally in Speagram we do function definitions like this: %P New function [syntax] as [type]. P% The syntax possibilities in Speagram are rich, but for Sasha we want just single strings to be used for function names. Let us create the right shorthand for function definitions with one argument. %P New function ''fun'' string ''('' string '':'' term type '')'' '':'' term type as syntax definition list. Let fun name ( var_name : arg_type ) : result_type be function ' ' name ' ' ' '(' ' arg_type ' ')' ' as result_type :: variable ' ' arg_name ' ' as arg_type :: []. P%
Done
Hide
Edit
Run
This part
New
Up
Down
Delete
Help
…
As you can see above Speagram can redefine it's own syntax. You have seen how to do this for function declarations, let us now do the same for rewrite rules. %P New function ?a ''=>'' ?a as input rewrite rule of ?a. New variable x1 as ?a. New variable x2 as ?a. Let x1 => x2 be let x1 be x2. P%
Done
Hide
Edit
Run
This part
New
Up
Down
Delete
Help
…
To make Sasha feel more like a programming language we added a few notational shorthands for variable definitions, standard type names and closing context. Read them below and figure out yourself what these do. %P New function ''var'' string '':'' term type as syntax definition. New variable s as string. New variable tt as term type. Let var s : tt be new variable ''s'' as tt. New function term type ''*'' term type as term type. New variable tt2 as term type. Let tt * tt2 be pair of tt and tt2. New function ''nat'' as term type. Let nat be natural number. New function ''bool'' as term type. Let bool be boolean. P%
Done
Hide
Edit
Run
This part
New
Up
Down
Delete
Help
…
To find the complete list of Sasha notations you should look inside the Speagram library inside the sasha file. But hopefully now you have an idea how functional programming language can be implemented on top of Speagram. One important thing that was not presented here is the full meta-functionality of Speagram, which can be used to implement more complex transformations. We skip this part for another tutorial.
Done
Hide
Edit
Run
This part
New
Up
Down
Delete
Help
…
Since we do not want to leave you just with the discussion of how Sasha is created on top of Speagram let us now use Sasha to write a program for converting logic formulas to conjunctive normal form (CNF). In our testsuite it is extended to compute prenex and Skolem normal forms as well. First we have to define the types of terms and formulas. %$ Class ''FO term''; ''VAR'' string is FO term; ''FUN'' string FO term list is FO term; $% As in any logic handbook, terms are either variables or are built with function symbols. Formulas on the other hand are built from predicates (PRED), negation, conjunctions and disjunctions over sequences (lists) of formulas and of course the universal (\A) and existential (\E) quantifier. %$ Class ''FO formula''; ''PRED'' string FO term list is FO formula; ''-'' FO formula is FO formula; ''/\'' FO formula list is FO formula; ''\/'' FO formula list is FO formula; ''\E'' string '':'' FO formula is FO formula; ''\A'' string '':'' FO formula is FO formula; $%
Done
Hide
Edit
Run
This part
New
Up
Down
Delete
Help
…
Let us start with a simple function that pushes the negations to the literals and thus computes the negation normal form. The auxiliary function negNNF computes just the NNF of the negation and we need it to map it to the list of formulas using the map function from the list module in the library. %$ fun NNF (f : FO formula) : FO formula; var x : string; var lf : FO formula list; fun negNNF (fo : FO formula) : FO formula; negNNF (fo) => NNF (- fo); NNF (- \E x : f) => \A x : NNF (- f); NNF (- \A x : f) => \E x : NNF (- f); NNF (- \/ lf) => /\ map negNNF ({}) to lf; NNF (- /\ lf) => \/ map negNNF ({}) to lf; NNF (/\ lf) => /\ map NNF ({}) to lf; NNF (\/ lf) => \/ map NNF ({}) to lf; NNF (\E x : f) => \E x : NNF (f); NNF (\A x : f) => \A x : NNF (f); NNF (-- f) => NNF (f); NNF (f) => f; ***; $%
Done
Hide
Edit
Run
This part
New
Up
Down
Delete
Help
…
We can now proceed to the function that computes the conjunctive normal form of a formula in NNF. We first create a function that returns the list of clauses and works only for formulas in NNF without quantifiers. %$ fun cnfList (f : FO formula) : FO formula list; fun disjOf (lf : FO formula list) : FO formula; disjOf (lf) => \/ lf; cnfList (/\ lf) => flatten map cnfList ({}) to lf; cnfList (\/ lf) => map disjOf ({}) to product of map cnfList ({}) to lf; cnfList (f) => [f]; ***; $% You should look closely at this function as it is central to computing CNF. For a conjunction it just computes the CNF of each formula and then concatenates all the lists together using the flatten function from the list library. In the case of a disjunction we need to take the product of all computed lists of clauses and make disjunction of each element of the result. Luckily the burden of computing the product is again put on the library and we only need to map an additional function that creates a disjunction. We can now finish the CNF implementation. %$ fun CNF (f : FO formula) : FO formula; var lf : FO formula list; CNF (\E x : f) => \E x : CNF (f); CNF (\A x : f) => \A x : CNF (f); CNF (\/ lf) => /\ cnfList (\/ lf); CNF (/\ lf) => /\ cnfList (/\ lf); CNF (f) => f; ***; $%
Done
Hide
Edit
Run
This part
New
Up
Down
Delete
Help
…
After this long trip in the direction of functional programming let us use our function and compute conjuntive normal forms of a few formulas (press "Run" to see the results) Compute CNF of (A /\ B) \/ (C /\ D). %$ CNF (\/ (/\ PRED "A" [], PRED "B" []), /\ (PRED "C" [], PRED "D" [])); $% Compute CNF of (not exists x : (P (x) /\ Q (x)). %$ CNF (- \E x : /\ PRED "P" [VAR "x"], PRED "Q" [VAR "x"]); $%
Saved XSLT Stylesheet
Saved SRGS Grammar